perm filename DIRTY[W82,JMC] blob
sn#646386 filedate 1982-03-12 generic text, type C, neo UTF8
COMMENT ⊗ VALID 00005 PAGES
C REC PAGE DESCRIPTION
C00001 00001
C00002 00002 dirty[w82,jmc] First order theory of dirty lisp
C00006 00003 questions
C00007 00004 Rules for converting dirty expressions to expressions with states
C00008 00005 cons
C00010 ENDMK
C⊗;
dirty[w82,jmc] First order theory of dirty lisp
A CLEAN EVAL FOR DIRTY LISP
Our object is a first order theory allowing
correctness proofs of dirty Lisp programs. Such programs may include
RPLACA, RPLACD and SETQs imbedded in functions. While they
are often written in functional form, their outputs are not related to their
inputs in the manner that the value of a function is related to the
values of its arguments. For example, replacing a subexpression by
one which has the same "value" will often change the "value" of the
whole expression.
copy u ← if null u then NIL
else {cons[car u, NIL]}[λz.copy1[z, z, cdr u]]
copy1[ans, w, v] ← if null v then ans
else copy1[ans, cdr rplacd[w, cons[car v,NIL]], cdr v]
copy[u,xi] ← if null u then NIL,xi
else {cons(CAR(u,xi),NIL,xi)}[λz xi1.copy1(z,z,CDR(u,xi1),xi1)]
copy1[ans,w,v,xi] ← if null z then ans,xi
else {cons(CAR(v,xi),NIL,xi)}[λx xi1.
{rplacd(w,x,xi1)}[λy xi2.
copy1[ans,CDR(y,xi2),CDR(v,xi2),xi2]
Since dirty Lisp programs change the machine state, a first
order theory must include the machine state explicitly. We denote the
machine state by xi often with subscripts.
val(e,xi) = if isvar e then c(e,xi),xi
else if car e = CAR
then {val(cadr e,xi)}[λx xi1.left c(x,xi1),xi1]
else if car e = CDR
then {val(cadr e,xi)}[λx xi1.right c(x,xi1),xi1]
else if car e = IF
then {val(cadr e,xi}[λx xi1.if x then val(caddr e,xi1)
else val(cadddr e,xi1)]
else if car e = CONS
then {val2(e,xi)}[λ x y xi1.right c(free,xi1),
a(free,right c(right c(free,xi1),x1),
a(right c(free,x1),comb(x,y),xi1))]
else if car e = RPLACD
then
We make the following abbreviations:
val1(e,xi) = val(cadr e,xi)
val2(e,xi) = {val1(e,xi)}[λx xi1.x,val(caddr e,xi1)]
val3(e,xi) = {val2(e,xi)}[λx y xi1.x,y,val(cadddr e,xi1)]
etc.
val(e,xi,a) = if isloc e then c(e,xi),xi
else if isvar e then cdr assoc(e,a),xi
else if car e = QUOTE then cadr e,xi
else if caar e = LAMBDA then
{val1 e}[λx xi1.val(adda e,xi1,cons(cons(adda e,x),a))]
questions
1. What to do about left-right evaluation order?
2. How to handle cons?
3. General rule for translation?
Rules for converting dirty expressions to expressions with states
f(g(x,y),h(u,v)) converts in general to
{g(x,y,xi)}[λa xi1.{h(u,v,xi1)}[λb xi2.f(a,b,xi2)]],
but if g leaves the state unchanged we can settle for
{h(u,v,xi)}[λb xi1.f(G(x,y,xi),b,xi1)].
cons
There are several level of detail at which cons can be treated. This
depends on whether we take into account the free storage list and whether
we take into account its finiteness and hence garbage collection.
Let's first consider a model in which we don't take the free storage
list into account, i.e. the new storage associated with a cons appears
to come from nowhere.
cons(x,y,xi) is a pair e,xi1 with the following properties:
1. CAR(e,xi1) = x ∧ CDR(e,xi1) = y, writeable as
1'. CAR(cons(x,y,xi)) = x ∧ CDR(cons(x,y,xi)) = y.
2. All previously existing registers point where they pointed before.
(This almost suggests that xi1 = xi, but I don't see how to say that.